g:IGroup, a, b:|g|. ~(a * b) = ((~(b)) * (~(a)))  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup
Definitions	t  T, x f y, x:A. B(x), P  Q, P & Q, P  Q, P  Q, IMonoid, IGroup
Lemmas	igrp wf, grp car wf, grp inv wf, grp op wf, grp op cancel l, grp inverse, mon assoc, grp id wf, grp inv assoc